@book{s7-200-manual,
        author = "{Siemens}",
        title = "S7-200 Programmable Controller System Manual",
        publisher = "Siemens",
        address = "",
        year = "2003"
}

@unpublished{cg_Coq_PLC,
        author = "Gang Chen",
        title = "The Verification and Analysis of {PLC} Programs Using Coq Proof Assistant",
        note = "Research Report RPT-2008-1, available at
        \texttt{www.lingcore.com/reports.html}",
}

@unpublished{cg_Coq_PLCII,
        author = "Hai Wan and Gang Chen and Xiaoyu Song and Ming Gu",
        title = "Formalization and Verification of {PLC} Timers in {C}oq",
        note = "Research Report RPT-2009-1",
}

@book{CoqArt,
        author = "Bertot, Yves and Cast\'eran, Pierre",
        title = "Interactive Theorem Proving and Program Development Coq'Art: The Calculus of Inductive Constructions",
        publisher = "Springer",
        year = "2004"
}

@book{IEEC61131-3,
        author = "{IEC International Standard 1131-3}",
        title = "Programmable Controllers, Part 3: Programming Languages",
        year = "1993"
}

@INPROCEEDINGS{Mader00aclassification,
    author = {Angelika Mader},
    title = {A classification of {PLC} models and applications},
    booktitle = {In WODES 2000: 5th Workshop on Discrete Event Systems},
    year = {2000},
    pages = {21--23},
    publisher = {Kluwer Academic Publishers}
}

@article{DBLP:journals/rts/KramerV97,
  author    = {Bernd J. Kr{\"a}mer and
               Norbert V{\"o}lker},
  title     = {A Highly Dependable Computing Architecture for Safety-Critical
               Control Applications},
  journal   = {Real-Time Systems},
  volume    = {13},
  number    = {3},
  year      = {1997},
  pages     = {237-251},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{ModellingPLCLV,
  author    = {I. Moon},
  title     = {Modelling programmable logic controllers for logic verification},
  journal   = {IEEE Control Systems Magazine},
  volume    = {14},
  number    = {2},
  year      = {1994},
  pages     = {53-59},
}

@INPROCEEDINGS{Mader99timedautomaton,
    author = {Angelika Mader and Hanno Wupper},
    title = {Timed automaton models for simple programmable logic controllers},
    booktitle = {Proceedings of the Euromicro Conference on Real-Time Systems},
    year = {1999},
    pages = {114--122},
    publisher = {IEEE Computer Society}
}

@inproceedings{ProvingSequentialFunctionChartProgramsUsingAutomata,
 author = {Dominique L'Her and Philippe Le Parc and Lionel Marc\'{e}},
 title = {Proving Sequential Function Chart Programs Using Automata},
 booktitle = {WIA '98: Revised Papers from  the Third International Workshop on Automata Implementation},
 year = {1999},
 isbn = {3-540-66652-4},
 pages = {149--163},
 publisher = {Springer-Verlag},
 address = {London, UK},
 }

@inproceedings{SynSignalModelPLC,
 author = {Fernando Jim\'{e}nez-Fraustro and Eric Rutten},
 title = {A Synchronous Model of IEC 61131 {PLC} Languages in SIGNAL},
 booktitle = {ECRTS '01: Proceedings of the 13th Euromicro Conference on Real-Time Systems},
 year = {2001},
 pages = {135},
 publisher = {IEEE Computer Society},
 address = {Washington, DC, USA},
 }


@article{dierks01plcautomata,
    author = "Henning Dierks",
    title = "{PLC}-automata: a new class of implementable real-time automata",
    journal = "Theoretical Computer Science",
    volume = "253",
    number = "1",
    pages = "61--93",
    year = "2001",
    url = "citeseer.ist.psu.edu/dierks97plcautomata.html" }

@MastersThesis{NBauer:Thesis:1998,
    author     =     {N. Bauer},
    title     =     {\"Ubersetzung von Steuerungsprogrammen in formale Modelle},
    school     =     {University of Dortmund},
    year     =     {1998},
}

@INPROCEEDINGS{Pnueli98translationvalidation,
    author = {A. Pnueli and M. Siegel and E. Singerman},
    title = {Translation validation},
    booktitle = {},
    year = {1998},
    pages = {151--166},
    publisher = {Springer}
}

@inproceedings{DBLP:conf/etfa/PollmacherZH05,
  author    = {D. Pollmacher and
               W. Zimmermann and
               Hans-Michael Hanisch},
  title     = {Translation validation for model-based code-generators for
               {PLCs}},
  booktitle = {ETFA},
  year      = {2005},
  ee        = {http://doi.ieeecomputersociety.org/10.1109/ETFA.2005.1612509},
  crossref  = {DBLP:conf/etfa/2005},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@book{HOLandHardwareVerification,
 author = {Melham,, T.},
 title = {Higher order logic and hardware verification},
 year = {1993},
 isbn = {0-521-41718-X},
 publisher = {Cambridge University Press},
 address = {New York, NY, USA},
 }

@inproceedings{KMR-ppdp2005,
Address = {New York, NY, USA},
Author = {Claude Kirchner and Pierre-Etienne Moreau and Antoine Reilles},
Booktitle = {PPDP '05: Proceedings of the 7th ACM SIGPLAN international conference on Principles and practice of declarative programming},
Pages = {187--197},
Publisher = {ACM Press},
Title = {Formal validation of pattern matching code},
Year = {2005}
}

@article{TV_in_OPT_COML,
 author = {Necula,, George C.},
 title = {Translation validation for an optimizing compiler},
 journal = {SIGPLAN Not.},
 volume = {35},
 number = {5},
 year = {2000},
 issn = {0362-1340},
 pages = {83--94},
 doi = {http://doi.acm.org/10.1145/358438.349314},
 publisher = {ACM},
 address = {New York, NY, USA},
 }

@article{TPM_TTS,
 author = {Henzinger,, Thomas A. and Manna,, Zohar and Pnueli,, Amir},
 title = {Temporal proof methodologies for timed transition systems},
 journal = {Inf. Comput.},
 volume = {112},
 number = {2},
 year = {1994},
 issn = {0890-5401},
 pages = {273--337},
 doi = {http://dx.doi.org/10.1006/inco.1994.1060},
 publisher = {Academic Press, Inc.},
 address = {Duluth, MN, USA},
 }

@inproceedings{AutomaticVericationMicroprecessor,
 author = {Burch,, Jerry R. and Dill,, David L.},
 title = {Automatic verification of Pipelined Microprocessor Control},
 booktitle = {CAV '94: Proceedings of the 6th International Conference on Computer Aided Verification},
 year = {1994},
 isbn = {3-540-58179-0},
 pages = {68--80},
 publisher = {Springer-Verlag},
 address = {London, UK},
 }

@article{GenericInterpreter,
 author = {Windley,, Phillip J.},
 title = {Formal Modeling and Verification of Microprocessors},
 journal = {IEEE Trans. Comput.},
 volume = {44},
 number = {1},
 year = {1995},
 issn = {0018-9340},
 pages = {54--72},
 doi = {http://dx.doi.org/10.1109/12.368009},
 publisher = {IEEE Computer Society},
 address = {Washington, DC, USA},
 }
